proctype delegate(byte myID) {

	byte K;
	byte chosenDelegates;
	byte myDrinkCount, wenchAcount, wenchBcount;
	int pubAcount, pubBcount;
	byte guardDrinkCount[N];
	byte dc;
	person outVote, inVote;
	byte from;
	bool amWench;
	bool guardIsWench;
	bool localIntoxicationView[N];
	mtype msg;

	if
	:: debug -> printf("DELEAGTE %d signing in\n", myID)
	:: else -> skip
	fi;
	
	for (K : 0 .. (N-1)) {
		localIntoxicationView[K] = false;
	}

/* ---------------------------------------------- */		
DELEGATE_LOOP:
/* ---------------------------------------------- */	

do
:: pubsVisited < N ->
	driverChannel!myID,ack;

if
	:: barrier1 -> skip
	:: terminate -> break
fi;


/* ---------------------------------------------- */	
FAIR_VOTE:
/* ---------------------------------------------- */	

if 
	:: isSmartDelegate || isDumbDelegate ->
	/* Decide with a coinflip and send out vote */
	COINFLIP(outVote.country);

	if
		:: debug -> printf("Delegate %d voting for pub %d\n", myID, outVote.country);
		:: else -> skip
	fi;

	for (K : 0 .. (N-1)) {
		channel[K]!myID,outVote;
	}


/* ---------------------------------------------- */	
SUBVERSIVE_VOTE:
/* ---------------------------------------------- */	

	:: isDumbGuard ->	
		/*Coin flip on each individual vote  */
		for(K : 0 .. (N-1)) {
		if
			:: outVote.country = pubA
			:: outVote.country = pubB
		fi;

		channel[K]!myID, outVote;
		}
		
	:: isSmartGuard ->
	
	/*Attempt to actually Split Delegates */
	for(K : 0 .. (N-1)) {
		if
			:: K % 2 == 0 -> outVote.country = pubA
			:: else -> outVote.country = pubB
		fi;
		channel[K]!myID, outVote;
		
	}

fi;

/* ---------------------------------------------- */	
DECIDE_VOTE:	
/* ---------------------------------------------- */	


if 
:: (accumulativeCounting) -> skip
:: else ->
	pubAcount = 0;
	pubBcount = 0;
fi;

/* Read all votes in and take majority */
if 
	:: isDumbDelegate ->
		for (K : 0 .. (N-1)) {
			channel[myID]?_,inVote;
			if
				:: inVote.country == pubA -> pubAcount++
				:: else -> pubBcount++
			fi;
		}
	
	:: isSmartDelegate ->

		for (K : 0 .. (N-1)) {
			channel[myID]?_,inVote;
			if 
			:: localIntoxicationView[K] -> skip;
				if
					:: debug -> printf("Delegate %d thinks deleagte %d is intoxicated\n", myID, K);
					:: else -> skip
				fi;
			:: else ->
				if
					:: inVote.country == pubA -> pubAcount++
					:: else -> pubBcount++
				fi;
			fi;
		}
		
	:: else -> 	for (K : 0 .. (N-1)) {
			channel[myID]?_,inVote;
		}

fi;

/* Go to the winning pub and tell driver we have arrived */
if
	:: pubAcount > pubBcount -> currentPub[myID] = pubA
	:: else -> currentPub[myID] = pubB
fi;
driverChannel!myID,ack;

if
	:: barrier2 -> skip
	:: terminate -> break
fi;

/* ---------------------------------------------- */	
PRE_WENCH_VOTE:
/* ---------------------------------------------- */	

if
	:: currentPub[myID] == myID -> goto MY_PUB
	:: else -> goto PRE_WENCH_VOTE_END
fi;

/* ---------------------------------------------- */	
MY_PUB:
/* ---------------------------------------------- */	

if
:: isDumbGuard ->
	/* Choose delegates randomly */
	atomic {
	
		select (K : 0 .. (N-1));
		wenchA.country = K;
		select (K : 0 .. 1);
		wenchB.country = K;
		wenchA.guard = false;
		wenchB.guard = false;
	
	}

:: isSmartGuard ->
	/* Choose two sober delegates if possible */
	chosenDelegates = 0;
	for (K : 0 .. (N-1)) {
		if
			:: intoxicated[K] -> skip
			:: else 
				if
				:: chosenDelegates == 0 -> wenchA.country = K;
				wenchA.guard = false;
				chosenDelegates++;
				:: chosenDelegates == 1 -> wenchB.country = K;
				wenchB.guard = false;
				chosenDelegates++;
				:: else -> skip
				fi;
		fi;
	}
	if
		:: chosenDelegates == 2 -> skip
		:: chosenDelegates == 1 ->
			select(K : 0 .. (N-1));
			wenchB.country = K;
			wenchB.guard = false;
		:: chosenDelegates == 0 ->
			select (K : 0 .. (N-1));
			wenchA.country = K;
			select (K : 0 .. 1);
			wenchB.country = K;
			wenchA.guard = false;
			wenchB.guard = false;
	fi;
	
:: else ->
	/* Choose the same as always */
	wenchA.country = 0;
	wenchA.guard = true;
	wenchB.country = 0;
	wenchB.guard = false;
	
fi;

/* ---------------------------------------------- */	
PRE_WENCH_VOTE_END:
/* ---------------------------------------------- */	


driverChannel!myID,ack;
if
	:: barrier3 -> skip
	:: terminate -> break
fi;



/* ---------------------------------------------- */	
WENCH_VOTE:
/* ---------------------------------------------- */	

if
	:: isSmartDelegate ->
	
	/* If the nominations are not as expected mark the local delegate as intoxicated */
	if
		:: !normalNomination -> localIntoxicationView[currentPub[myID]] = true;
		:: else -> skip
	fi;
	
	:: else -> skip

fi;

if

	:: isSmartDelegate ->
	
		if
			:: wenchA.guard && !wenchB.guard ->
				outVote.country = wenchA.country;
				outVote.guard = wenchA.guard;
			:: wenchB.guard && !wenchA.guard ->
				outVote.country = wenchB.country;
				outVote.guard = wenchB.guard;
			:: else ->
				if
					:: wenchA.country < wenchB.country ->
						outVote.country = wenchA.country;
						outVote.guard = wenchA.guard;
					:: else ->
						outVote.country = wenchB.country;
						outVote.guard = wenchB.guard;
				fi;
		fi;
				
	:: isDumbDelegate ->

	/* Use a coin flip */
	if
		:: true ->
			outVote.country = wenchA.country;
			outVote.guard = wenchA.guard;
		:: true ->
			outVote.country = wenchB.country;
			outVote.guard = wenchB.guard;
	fi;

	:: else -> skip

fi;

/* Send out votes for the wench */
for (K : 0 .. (N-1)) {

	if
		:: isDumbGuard ->
			/* Use a coin flip */
			if
				:: true ->
					outVote.country = wenchA.country;
					outVote.guard = wenchA.guard;
				:: true ->
					outVote.country = wenchB.country;
					outVote.guard = wenchB.guard;
			fi;
		:: isSmartGuard ->
			if
				:: K % 2 == 0 ->
					outVote.country = wenchA.country;
					outVote.guard = wenchA.guard;
				:: else ->
					outVote.country = wenchB.country;
					outVote.guard = wenchB.guard;
			fi;
		:: else -> skip
	fi;
	channel[K]!myID,outVote, guardDrinkCount[myID];
}

/* ---------------------------------------------- */	
DECIDE_WENCH_VOTE:
/* ---------------------------------------------- */

/* Read in votes for the wench */


wenchAcount = 0;
wenchBcount = 0;

amWench = false;
guardIsWench = false;

if
/* if we are involved in the election take count of the votes */
:: wenchA.country == myID || wenchB.country == myID ->
	
	if
	/* Smart delegates try to learn who is intoxicated */
	:: isSmartDelegate ->
		for(K : 0 .. (N-1)) {
			channel[myID]?from,inVote;
			if 
			:: !expectedVote -> localIntoxicationView[from] = true;
			:: else ->
				if
				:: isWenchA -> wenchAcount++
				:: isWenchB -> wenchBcount++
				fi;
			fi;
		}
		
	/* Dumb delegates do not */
	:: isDumbDelegate ->
		for(K : 0 .. (N-1)) {
			channel[myID]?from,inVote;
			if
			:: isWenchA -> wenchAcount++
			:: isWenchB -> wenchBcount++
			fi;
		}
		
	/* Guards learn the drink count of all the other guards */
	:: else -> 
		for(K : 0 .. (N-1)) {
			channel[myID]?from, inVote, dc;
			guardDrinkCount[from] = dc;
		}
	fi;

	if 
	/* Smart delegates attempt to choose a bodyguard count the votes */
	:: isSmartDelegate ->
		if 
		/* If both wenches are guards then wenchA will be elected */
		:: wenchA.guard && wenchB.guard ->
			if
			:: wenchA.country == myID -> guardIsWench = true
			:: else -> skip
			fi;
		/* If only one wench is a guard then the guard will be elected */
		:: wenchA.guard && !wenchB.guard && wenchA.country == myID -> guardIsWench = true
		:: wenchB.guard && !wenchA.guard && wenchB.country == myID -> guardIsWench = true
		/* If both nominations are delegates wenchA will be elected */
		:: wenchA.country == myID -> amWench = true
		:: else -> skip
	fi;
	/* Dumb delegates take majority */
	:: isDumbDelegate -> 
		if
		/* Wench A was elected */
		:: wenchAcount > wenchBcount ->
			if
			:: wenchA.country == myID && wenchA.guard -> guardIsWench = true
			:: wenchA.country == myID && !wenchA.guard -> amWench = true
			:: else -> skip
			fi;
		/* Wench B was elected */
		:: else ->
			if
			:: wenchB.country == myID && wenchB.guard -> guardIsWench = true;
			:: wenchB.country == myID && !wenchB.guard -> amWench = true;
			:: else -> skip
			fi;
		fi;
			
	:: else ->	
		if 
		:: isSmartGuard ->
			/* If both guards are elected choose the guard with the lowest drink count */
			if 
			:: wenchA.guard && wenchB.guard ->
				if 
				:: wenchA.country == myID && guardDrinkCount[wenchA.country] < guardDrinkCount[wenchB.country] ->
					 guardIsWench = true;
				:: wenchB.country == myID && guardDrinkCount[wenchB.country] <= guardDrinkCount[wenchA.country] ->
					 guardIsWench = true;
				:: else -> skip
				fi;
			/* If my delegate was nominated pretend he win */
			:: else -> 
				if 
				:: wenchA.country == myID && !wenchA.guard -> amWench = true
				:: wenchB.country == myID && !wenchB.guard -> amWench = true
				:: else -> skip /* Elect no one */
				fi;
			fi;
		 
		:: isDumbGuard ->
			/* If both are guards let wenchA take the fall */
			if 
			:: wenchA.guard && wenchB.guard ->
				if 
				:: wenchA.country == myID -> guardIsWench = true;
				:: else -> skip
				fi;
			/* If my delegate was nominated pretend he win */
			:: else -> 
				if
				:: wenchA.country == myID && !wenchA.guard -> amWench = true
				:: wenchB.country == myID && !wenchB.guard -> amWench = true
				:: else -> skip /* Elect no one */
				fi;
			fi;
		fi;
	fi;
	
	/* Not involved in the election .. clear channel */
:: else ->
	for (K : 0 .. (N-1)) {
		channel[myID]?_,_;
	}
fi;

/* Let the driver know */
if
	:: amWench -> driverChannel!myID,dwench;
	:: guardIsWench -> driverChannel!myID,gwench;
	:: else -> driverChannel!myID,ack;
fi;

/* Get the result */
drinkChannel[myID]?_,msg;

if
	:: msg == dwench -> amWench = true; guardIsWench = false;
	:: msg == gwench -> amWench = false; guardIsWench = true; 
	:: else -> amWench = false; guardIsWench = false;
	
fi;

if
	:: barrier4 -> skip
	:: terminate -> break
fi;

/* ---------------------------------------------- */	
SERVING_ROUND:
/* ---------------------------------------------- */


/* If we are a server, serve drinks */
if
	:: guardIsWench || amWench ->
		/* Serve a round of drinks */
		for (K : 0 .. (N-1)) {
			drinkChannel[K]!myID,drink;
		}
		
		/* Drink our drink and any returned drinks */
		for (K : 0 .. (N-1)) {
			drinkChannel[myID]?from,msg;
			if
				:: msg == drink && !intoxicated[myID] ->
				if :: amWench -> myDrinkCount++;
						if :: myDrinkCount > p -> intoxicated[myID] = true
							 :: myDrinkCount > p -> skip
							 :: else -> skip
						fi;
						:: guardIsWench && (from != myID) -> guardDrinkCount[myID]++;
						printf("GUARD IS DRINKING\n");
						if :: guardDrinkCount[myID] > b -> guardIntoxicated = true
							 :: guardDrinkCount[myID] > b -> skip
							 :: else -> skip
						fi;
						:: else -> skip
				fi;
				:: else -> skip
			fi;
		}
	
	
	/* If we are not the server drink or return our drink */	
	:: else ->
		drinkChannel[myID]?from,eval(drink);
		if
			:: intoxicated[myID] -> drinkChannel[from]!myID,drink;
			:: else -> drinkChannel[from]!myID,ack;
				myDrinkCount++;
				if :: myDrinkCount > p -> intoxicated[myID] = true
					 :: myDrinkCount > p -> skip
					 :: else -> skip
				fi;
		fi;
fi;

driverChannel!myID,ack;
if
	:: barrier5 -> skip
	:: terminate -> break
fi;


/* ---------------------------------------------- */	
DELEGATE_LOOP_END:
/* ---------------------------------------------- */	

:: else -> break;
od;



if
:: debug -> printf("DELEGATE %d SIGNING OUT\n", myID);
:: else -> skip
fi
}